Lambda the Ultimate

The video and slides of David Pollak's BayFP presentation on lift are available online.

While the thrust of the talk is on lift as a web framework, you get a very nice intro to Scala along the way, and David even mentions a quick way to get a PLT PhD, for those interested in that sort of thing...

(via the TYPES Forum)

R6RS includes an operational semantics for a large portion of the language including unspecified order of evaluation, continuations and dynamic-wind, multiple values, quote, exceptions, eqv, letrec, etc. (the only major, missing features are macros and the numeric tower). The semantics are Felleisen/Hieb-style reduction semantics and are implemented in PLT Redex.

A draft JFP paper describing operational semantics for R5RS and the reduction systems themselves are both available online courtesy of Jacob Matthews and Robert Findler.

Generative Code Specialisation for High-Performance Monte Carlo Simulations (Don Stewart, Hugh Chaffey-Millar, Gabriele Keller, Manuel M. T. Chakravarty and Christopher Barner-Kowollik) is a nice example of exploiting PL theory techniques (relevant keywords highlighted below) to combine a need for generality with high performance, to achieve outstanding results:

We address the tension between software generality and performance in the domain of scientific and financial simulations based on Monte-Carlo methods. To this end, we present a novel software architecture, centred around the concept of a specialising simulator generator, that combines and extends methods from generative programming, partial evaluation, runtime code generation, and dynamic code loading. The core tenet is that, given a fixed simulator configuration, a generator in a functional language can produce low-level code that is more highly optimised than a manually implemented generic simulator. We also introduce a skeleton, or template, capturing a wide range of Monte-Carlo methods and use it to explain how to design specialising simulator generators and how to generate parallelised simulators for multi-core and distributed-memory multiprocessors.

We evaluated the practical benefits and limitations of our approach by applying it to a highly relevant problem in computational chemistry. More precisely, we used a Markov-chain Monte-Carlo method for the study of advanced forms of polymerisation kinetics. The resulting implementation executes faster than all competing software products, while at the same time also being more general. The generative architecture allows us to cover a wider range of chemical reactions and to target a wider range of high-performance architectures (such as PC clusters and SMP multiprocessors).

We show that it is possible to outperform low-level languages with functional programming in domains with very stringent performance requirements if the domain also demands generality.

The project web site provides the Haskell and C source. The Haskell code generates specialized C code for specific simulations, which is then compiled and dynamically loaded.

To quote Richard Zach:

CSLI Lecture Notes are now part of the Stanford Medieval and Modern Thought Digitization Project. That means books such as Unger's Cut-elimination, Normalization, and the Theory of Proofs, Troelstra's Lectures on Linear Logic, Aczel's Non-well-founded Sets, van Benthem's Manual of Intensional Logic, and Goldblatt's Logics of Time and Computation are now available online and for free. (HT: Shawn)

Also of interest here will be McCarthy's Defending AI research, and Modal logic and process algebra : a bisimulation perspective, edited by Venema, de Rijke and Ponse.

NEXCEL, a Deductive Spreadsheet, Iliano Cervesato. 2006.

Usability and usefulness have made the spreadsheet one of the most successful computing applications of all times: millions rely on it every day for anything from typing grocery lists to developing multimillion dollar budgets. One thing spreadsheets are not very good at is manipulating symbolic data and helping users make decisions based on them. By tapping into recent research in Logic Programming, Databases and Cognitive Psychology, we propose a deductive extension to the spreadsheet paradigm which addresses precisely this issue. The accompanying tool, which we call NEXCEL, is intended as an automated assistant for the daily reasoning and decision-making needs of computer users, in the same way as a spreadsheet application such as Microsoft Excel assists them every day with calculations simple and complex. Users without formal training in Logic or even Computer Science can interactively define logical rules in the same simple way as they define formulas in Excel. NEXCEL immediately evaluates these rules thereby returning lists of values that satisfy them, again just like with numerical formulas. The deductive component is seamlessly integrated into the traditional spreadsheet so that a user not only still has access to the usual functionalities, but is able to use them as part of the logical inference and, dually, to embed deductive steps in a numerical calculation.

This is a neat paper about using Datalog-style relations to extend spreadsheets with some deductive database features. It seems like Datalog represents a real sweet spot in the design space for logic programming -- I've seen a lot of people put it to effective use.

Ben Laurie:

I’ve been running a team at Google for a while now, implementing capabilities in Javascript....a Caja program will run without modification on a standard Javascript interpreter - though it won’t be secure, of course! When it is compiled then, like CaPerl, the result is standard Javascript that enforces capability security. What does this mean? It means that Web apps can embed untrusted third party code without concern that it might compromise either the application’s or the user’s security...I’m very excited about this project and the involvement of some world class capability experts, including Mark Miller (of E fame) who is a full-time member of the Caja development team.

This could possibly be a very important development. I haven't delved into Caja, but I know some members know all there is to know, so perhaps they can enlighten us about the details...

Markus Gaelli, Oscar Nierstrasz, Serge Stinckwich. Idioms for Composing Games with Etoys. C5'06.

Creating one’s own games has been the main motivation for many people to learn programming. But the barrier to learn a general purpose programming language is very high, especially if some positive results can only be expected after having manually written more than 100 lines of code. With this paper we first motivate potential users by showing that one can create classic board- and arcade games like Lights Out, TicTacToe, or Pacman within the playful and constructivist visual learning environment EToys dragging together only a few lines of code. Then we present recurring idioms which helped to develop these games with only a few lines of code.

Learning to program with Etoys is very mind-stretching. Beyond the drag-and-drop syntax there's a world where programs are created by directly manipulating tangible objects on the screen. The objects expose a varied collection of primitives and it's a real journey of discovery to learn how to compose simple and beautiful programs. This paper documents some of the "aha!" discoveries that make Etoys programming lots of fun.

The Etoys end-user programming environment is becoming tremendously important because of its inclusion with the One Laptop Per Child XO. Etoys was invented by Alan Kay's research group and is in continuous development and use as an integrated feature of Squeak Smalltalk. The Squeak/Etoys community includes lots of researchers, programmers, teachers, and kids around the world.

Squeaky Tales is a series of short tutorial screencasts designed to each people to program with Etoys. I'm very excited that this may be what's needed to make Etoys programming easy to learn for people at home. My experience has been that it's easy and fun to teach Etoys programming face-to-face with everybody using their own laptop, but that it's very slow and frustrating to try and learn Etoys by yourself just by installing it and clicking around. If Squeaky Tales makes it easy and fun to learn Etoys all by yourself at home then it's quite a contribution to the world!

If you try learning Etoys with Squeaky Tales then do leave a comment to say how you get along!

Vaidas Gasiunas, Mira Mezini, Klaus Ostermann. Dependent Classes. OOPSLA'07.

Virtual classes allow nested classes to be refined in subclasses. In this way nested classes can be seen as dependent abstractions of the objects of the enclosing classes. Expressing dependency via nesting, however, has two limitations: Abstractions that depend on more than one object cannot be modeled and a class must know all classes that depend on its objects. This paper presents dependent classes, a generalization of virtual classes that expresses similar semantics by parameterization rather than by nesting. This increases expressivity of class variations as well as the flexibility of their modularization. Besides, dependent classes complement multimethods in scenarios where multi-dispatched abstractions rather than multi-dispatched methods are needed. They can also be used to express more precise signatures of multimethods and even extend their dispatch semantics. We present a formal semantics of dependent classes and a machine-checked type soundness proof in Isabelle/HOL, the first of this kind for a language with virtual classes and path-dependent types.

I enjoyed this talk at OOPSLA, although I was not able to see the end, and I enjoyed the paper even more. There's been so much work on virtual classes in recent years, and while I very clearly see a strong practical motivation for this work, I admit that I find it difficult to keep track of the technical trade-offs between different approaches. This, plus the persistent limitations mentioned in the abstract, lends some of the papers an unfortunately tedious feel (to me). I find this work refreshing, since it introduces a substantial new idea in this area. (And of course, one of the authors posts here regularly...)

There's a new document on the incompatibilities between ECMAScript Edition 3 and the proposed Edition 4. Given the recent controversy in the blogosphere and the degree of interest in last week's discussion of the proposed ES4, this document may be of interest to LtUers.

It's also interesting to think of conservative extension not as an all-or-nothing property, but to judge incompatibilities in terms of their impact. This document attempts to enumerate and classify the different ways the proposed ES4 spec conflicts with the specification of ES3.

(One last note: there's a new pre-release of the reference implementation available, with binaries for all major platforms. Check it out!)